strong_safety(T;tr.P(tr)) == tr1, tr2:T List. tr1  tr2  P(tr2)  P(tr1) 

latex

---

clarification:

strong_safety(T;tr.P(tr)) == tr1:T List, tr2:T List. sublist(T; tr1; tr2)  P(tr2)  P(tr1) 

latex

Definitions	x:A. B(x), L1  L2, P  Q
FDL editor aliases	strong_safety